<!DOCTYPE html>
<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width">
<meta name="theme-color" content="#222"><meta name="generator" content="Hexo 6.3.0">

  <link rel="apple-touch-icon" sizes="180x180" href="/blog/images/apple-touch-icon-next.png">
  <link rel="icon" type="image/png" sizes="32x32" href="/blog/images/Horse.png">
  <link rel="icon" type="image/png" sizes="16x16" href="/blog/images/Horse.png">
  <link rel="mask-icon" href="/blog/images/logo.svg" color="#222">

<link rel="stylesheet" href="/blog/css/main.css">



<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.0/css/all.min.css" integrity="sha256-HtsXJanqjKTc8vVQjO4YMhiqFoXkfBsjBWcX91T1jr8=" crossorigin="anonymous">
  <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.css" integrity="sha256-Vzbj7sDDS/woiFS3uNKo8eIuni59rjyNGtXfstRzStA=" crossorigin="anonymous">

<script class="next-config" data-name="main" type="application/json">{"hostname":"yanlwsometing.gitee.io","root":"/blog/","images":"/blog/images","scheme":"Pisces","darkmode":false,"version":"8.16.0","exturl":false,"sidebar":{"position":"left","display":"post","padding":18,"offset":12},"copycode":{"enable":true,"show_result":true,"style":"flat"},"bookmark":{"enable":false,"color":"#222","save":"auto"},"mediumzoom":false,"lazyload":false,"pangu":false,"comments":{"style":"tabs","active":null,"storage":true,"lazyload":false,"nav":null},"stickytabs":false,"motion":{"enable":false,"async":false,"transition":{"menu_item":"fadeInDown","post_block":"fadeIn","post_header":"fadeInDown","post_body":"fadeInDown","coll_header":"fadeInLeft","sidebar":"fadeInUp"}},"prism":false,"i18n":{"placeholder":"搜索...","empty":"没有找到任何搜索结果：${query}","hits_time":"找到 ${hits} 个搜索结果（用时 ${time} 毫秒）","hits":"找到 ${hits} 个搜索结果"}}</script><script src="/blog/js/config.js"></script>

    <meta name="description" content="前言在前面的学习中，我们证明了大量的命题：*’相等性命题’*（e1 &#x3D; e2）、蕴含式（P → Q）和量化命题 （∀ x, P x），在本章中，我们将会看到如何用 Coq 解决类似形式的逻辑推理。 对于*命题(Prop)*，有这如下的特点：  所有语法形式良好的命题，无论是否为真，其类型均为 Prop  命题还是*’一等的（First-Class）’*实体， 即在 Coq 的世界中，我们">
<meta property="og:type" content="article">
<meta property="og:title" content="SF-1-Logic">
<meta property="og:url" content="https://yanlwsometing.gitee.io/blog/2023/07/22/SF-1-Logic/index.html">
<meta property="og:site_name" content="yanlwsometing">
<meta property="og:description" content="前言在前面的学习中，我们证明了大量的命题：*’相等性命题’*（e1 &#x3D; e2）、蕴含式（P → Q）和量化命题 （∀ x, P x），在本章中，我们将会看到如何用 Coq 解决类似形式的逻辑推理。 对于*命题(Prop)*，有这如下的特点：  所有语法形式良好的命题，无论是否为真，其类型均为 Prop  命题还是*’一等的（First-Class）’*实体， 即在 Coq 的世界中，我们">
<meta property="og:locale" content="zh_CN">
<meta property="article:published_time" content="2023-07-22T02:43:43.000Z">
<meta property="article:modified_time" content="2023-12-15T09:08:34.190Z">
<meta property="article:author" content="yanlw">
<meta property="article:tag" content="博客">
<meta name="twitter:card" content="summary">


<link rel="canonical" href="https://yanlwsometing.gitee.io/blog/2023/07/22/SF-1-Logic/">



<script class="next-config" data-name="page" type="application/json">{"sidebar":"","isHome":false,"isPost":true,"lang":"zh-CN","comments":true,"permalink":"https://yanlwsometing.gitee.io/blog/2023/07/22/SF-1-Logic/","path":"2023/07/22/SF-1-Logic/","title":"SF-1-Logic"}</script>

<script class="next-config" data-name="calendar" type="application/json">""</script>
<title>SF-1-Logic | yanlwsometing</title>
  








  <noscript>
    <link rel="stylesheet" href="/blog/css/noscript.css">
  </noscript>
</head>

<body itemscope itemtype="http://schema.org/WebPage">
  <div class="headband"></div>

  <main class="main">
    <div class="column">
      <header class="header" itemscope itemtype="http://schema.org/WPHeader"><div class="site-brand-container">
  <div class="site-nav-toggle">
    <div class="toggle" aria-label="切换导航栏" role="button">
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
    </div>
  </div>

  <div class="site-meta">

    <a href="/blog/" class="brand" rel="start">
      <i class="logo-line"></i>
      <p class="site-title">yanlwsometing</p>
      <i class="logo-line"></i>
    </a>
  </div>

  <div class="site-nav-right">
    <div class="toggle popup-trigger" aria-label="搜索" role="button">
    </div>
  </div>
</div>



<nav class="site-nav">
  <ul class="main-menu menu"><li class="menu-item menu-item-home"><a href="/blog/" rel="section"><i class="fa fa-home fa-fw"></i>首页</a></li><li class="menu-item menu-item-tags"><a href="/blog/tags/" rel="section"><i class="fa fa-tags fa-fw"></i>标签</a></li><li class="menu-item menu-item-categories"><a href="/blog/categories/" rel="section"><i class="fa fa-th fa-fw"></i>分类</a></li><li class="menu-item menu-item-archives"><a href="/blog/archives/" rel="section"><i class="fa fa-archive fa-fw"></i>归档</a></li><li class="menu-item menu-item-commonweal"><a href="/blog/404/" rel="section"><i class="fa fa-heartbeat fa-fw"></i>公益 404</a></li>
  </ul>
</nav>




</header>
        
  
  <aside class="sidebar">

    <div class="sidebar-inner sidebar-nav-active sidebar-toc-active">
      <ul class="sidebar-nav">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <div class="sidebar-panel-container">
        <!--noindex-->
        <div class="post-toc-wrap sidebar-panel">
            <div class="post-toc animated"><ol class="nav"><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%89%8D%E8%A8%80"><span class="nav-number">1.</span> <span class="nav-text">前言</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E9%80%BB%E8%BE%91%E8%81%94%E7%BB%93%E8%AF%8D"><span class="nav-number">2.</span> <span class="nav-text">逻辑联结词</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-%E5%90%88%E5%8F%96"><span class="nav-number">2.1.</span> <span class="nav-text">1. 合取</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-%E6%9E%90%E5%8F%96"><span class="nav-number">2.2.</span> <span class="nav-text">2. 析取</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-%E5%81%87%E5%91%BD%E9%A2%98%E4%B8%8E%E5%90%A6%E5%AE%9A"><span class="nav-number">2.3.</span> <span class="nav-text">3. 假命题与否定</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#4-%E7%9C%9F%E5%80%BC"><span class="nav-number">2.4.</span> <span class="nav-text">4. 真值</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#5-%E9%80%BB%E8%BE%91%E7%AD%89%E4%BB%B7"><span class="nav-number">2.5.</span> <span class="nav-text">5. 逻辑等价</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#6-%E5%B9%BF%E9%9B%86%E4%B8%8E%E9%80%BB%E8%BE%91%E7%AD%89%E4%BB%B7"><span class="nav-number">2.6.</span> <span class="nav-text">6. 广集与逻辑等价</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#7-%E5%AD%98%E5%9C%A8%E9%87%8F%E5%8C%96"><span class="nav-number">2.7.</span> <span class="nav-text">7. 存在量化</span></a></li></ol></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E4%BD%BF%E7%94%A8%E5%91%BD%E9%A2%98%E7%BC%96%E7%A8%8B"><span class="nav-number">3.</span> <span class="nav-text">使用命题编程</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%AF%B9%E5%8F%82%E6%95%B0%E5%BA%94%E7%94%A8%E5%AE%9A%E7%90%86"><span class="nav-number">4.</span> <span class="nav-text">对参数应用定理</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Coq-vs-%E6%9E%84%E9%80%A0%E9%80%BB%E8%BE%91"><span class="nav-number">5.</span> <span class="nav-text">Coq vs. 构造逻辑</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-%E5%87%BD%E6%95%B0%E7%9A%84%E5%A4%96%E5%BB%B6%E6%80%A7"><span class="nav-number">5.1.</span> <span class="nav-text">1. 函数的外延性</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-%E5%91%BD%E9%A2%98-vs-%E5%B8%83%E5%B0%94%E5%80%BC"><span class="nav-number">5.2.</span> <span class="nav-text">2. 命题 vs. 布尔值</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-%E7%BB%8F%E5%85%B8%E9%80%BB%E8%BE%91-vs-%E6%9E%84%E9%80%A0%E9%80%BB%E8%BE%91"><span class="nav-number">5.3.</span> <span class="nav-text">3. 经典逻辑 vs. 构造逻辑</span></a></li></ol></li></ol></div>
        </div>
        <!--/noindex-->

        <div class="site-overview-wrap sidebar-panel">
          <div class="site-author animated" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image" alt="yanlw"
      src="/blog/images/avatar.jpg">
  <p class="site-author-name" itemprop="name">yanlw</p>
  <div class="site-description" itemprop="description">穷则独善其身，达则兼济天下！</div>
</div>
<div class="site-state-wrap animated">
  <nav class="site-state">
      <div class="site-state-item site-state-posts">
        <a href="/blog/archives/">
          <span class="site-state-item-count">23</span>
          <span class="site-state-item-name">日志</span>
        </a>
      </div>
      <div class="site-state-item site-state-categories">
          <a href="/blog/categories/">
        <span class="site-state-item-count">9</span>
        <span class="site-state-item-name">分类</span></a>
      </div>
      <div class="site-state-item site-state-tags">
          <a href="/blog/tags/">
        <span class="site-state-item-count">18</span>
        <span class="site-state-item-name">标签</span></a>
      </div>
  </nav>
</div>
  <div class="links-of-author animated">
      <span class="links-of-author-item">
        <a href="https://gitee.com/yanlwsometing" title="Gitee → https:&#x2F;&#x2F;gitee.com&#x2F;yanlwsometing" rel="noopener me" target="_blank"><i class="fab fa-gitee fa-fw"></i>Gitee</a>
      </span>
      <span class="links-of-author-item">
        <a href="mailto:1977712019@qq.com" title="Mail → mailto:1977712019@qq.com" rel="noopener me" target="_blank"><i class="fa fa-envelope fa-fw"></i>Mail</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://weibo.com/" title="Weibo → https:&#x2F;&#x2F;weibo.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-weibo fa-fw"></i>Weibo</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://twitter.com/" title="Twitter → https:&#x2F;&#x2F;twitter.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-twitter fa-fw"></i>Twitter</a>
      </span>
  </div>

        </div>
      </div>
        <div class="back-to-top animated" role="button" aria-label="返回顶部">
          <i class="fa fa-arrow-up"></i>
          <span>0%</span>
        </div>
    </div>

    
  </aside>


    </div>

    <div class="main-inner post posts-expand">


  


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="zh-CN">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/07/22/SF-1-Logic/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="SF-1-Logic | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h1 class="post-title" itemprop="name headline">
          SF-1-Logic
        </h1>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-07-22 10:43:43" itemprop="dateCreated datePublished" datetime="2023-07-22T10:43:43+08:00">2023-07-22</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:34" itemprop="dateModified" datetime="2023-12-15T17:08:34+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Coq/" itemprop="url" rel="index"><span itemprop="name">Coq</span></a>
        </span>
    </span>

  
    <span class="post-meta-item" title="阅读次数" id="busuanzi_container_page_pv">
      <span class="post-meta-item-icon">
        <i class="far fa-eye"></i>
      </span>
      <span class="post-meta-item-text">阅读次数：</span>
      <span id="busuanzi_value_page_pv"></span>
    </span>
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody"><h2 id="前言"><a href="#前言" class="headerlink" title="前言"></a>前言</h2><p>在前面的学习中，我们证明了大量的命题：*’相等性命题’*（e1 &#x3D; e2）、蕴含式（P → Q）和量化命题 （∀ x, P x），在本章中，我们将会看到如何用 Coq 解决类似形式的逻辑推理。</p>
<p>对于*命题(Prop)*，有这如下的特点：</p>
<ul>
<li><p>所有语法形式良好的命题，无论是否为真，其类型均为 Prop</p>
</li>
<li><p>命题还是*’一等的（First-Class）’*实体， 即在 Coq 的世界中，我们可以像操作其它实体那样操作命题</p>
</li>
<li><p>命题可既以出现在 Theorem（还有 Lemma 以及 Example）的声明中，也可以用 Definition 为命题取名，之后我们可以在任何需要此命题的地方使用它们名字</p>
</li>
<li><p>*’参数化’*的命题 – 也就是一个接受某些类型的参数， 然后返回一个命题的函数</p>
<span id="more"></span></li>
</ul>
<h2 id="逻辑联结词"><a href="#逻辑联结词" class="headerlink" title="逻辑联结词"></a>逻辑联结词</h2><h3 id="1-合取"><a href="#1-合取" class="headerlink" title="1. 合取"></a>1. 合取</h3><p>命题 A 与 B 的*’合取’<em>（即</em>‘逻辑与’*）写作 A ∧ B，表示一个 A 与 B 均为真的断言。</p>
<p>证明合取的命题通常使用 split 策略。它会分别为语句的两部分生成两个子目标：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Example and_example : 3 + 4 = 7 /\ 2 * 2 = 4.</span><br><span class="line"></span><br><span class="line">Proof.</span><br><span class="line">  split.</span><br><span class="line">  - (* 3 + 4 = 7 *) reflexivity.</span><br><span class="line">  - (* 2 * 2 = 4 *) reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>如果当前证明上下文中存在形如 A ∧ B 的前提 H，那么 destruct H as [HA HB] 将会从上下文中移除 H 并增加 HA 和 HB 两个新的前提：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br></pre></td><td class="code"><pre><span class="line">Lemma and_example2 :</span><br><span class="line">  forall n m : nat, n = 0 /\ m = 0 -&gt; n + m = 0.</span><br><span class="line">Proof.</span><br><span class="line">  (* WORKED IN CLASS *)</span><br><span class="line">  intros n m H.</span><br><span class="line">  destruct H as [Hn Hm].</span><br><span class="line">  rewrite Hn. rewrite Hm.</span><br><span class="line">  reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>也可以在引入 H 的同时对其进行解构：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Lemma and_example2&#x27; :</span><br><span class="line">  forall n m : nat, n = 0 /\ m = 0 -&gt; n + m = 0.</span><br><span class="line">Proof.</span><br><span class="line">  intros n m [Hn Hm].</span><br><span class="line">  rewrite Hn. rewrite Hm.</span><br><span class="line">  reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>当某些上下文中只需要合取的一部分时，可以用 destruct 进行解构（或许是作为 intros 的一部分）并用下划线模式 _ 来丢弃不需要的合取分式</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Lemma and_example2&#x27; :</span><br><span class="line">  forall n m : nat, n = 0 /\ m = 0 -&gt; n + m = 0.</span><br><span class="line">Proof.</span><br><span class="line">  intros n m [Hn _].</span><br><span class="line">  rewrite Hn. rewrite Hm.</span><br><span class="line">  reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>顺便一提，中缀记法 ∧ 只是 and A B 的语法糖而已； and 是 Coq 中将两个命题合并成一个命题的运算符</p>
<h3 id="2-析取"><a href="#2-析取" class="headerlink" title="2. 析取"></a>2. 析取</h3><p><em>析取</em>，即两个命题的*’逻辑或’*：若 A 或 B 二者之一为真，则 A ∨ B 为真。（这种中缀记法表示 or A B，其中 or : Prop → Prop → Prop。</p>
<p>证明某个析取命题成立，只需证明其任意一边的命题成立就够了。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br></pre></td><td class="code"><pre><span class="line">Lemma or_intro_l : forall A B : Prop, A -&gt; A \/ B.</span><br><span class="line">Proof.</span><br><span class="line">  intros A B HA.</span><br><span class="line">  left.</span><br><span class="line">  apply HA.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>在证明中使用析取前提，我们需要分类讨论，可以显式地通过 destruct 或隐式地通过 intros 模式来拆分：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br></pre></td><td class="code"><pre><span class="line">Lemma factor_is_O:</span><br><span class="line">  forall n m : nat, n = 0 \/ m = 0 -&gt; n * m = 0.</span><br><span class="line">Proof.</span><br><span class="line">  (* This pattern implicitly does case analysis on</span><br><span class="line">     [n = 0 \/ m = 0] *)</span><br><span class="line">  intros n m [Hn | Hm].</span><br><span class="line">  - (* Here, [n = 0] *)</span><br><span class="line">    rewrite Hn. reflexivity.</span><br><span class="line">  - (* Here, [m = 0] *)</span><br><span class="line">    rewrite Hm. rewrite &lt;- mult_n_O.</span><br><span class="line">    reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>



<h3 id="3-假命题与否定"><a href="#3-假命题与否定" class="headerlink" title="3. 假命题与否定"></a>3. 假命题与否定</h3><p>Coq能证明某些东西是*’真’<em>的，也能证明某些给定的命题</em>‘不是’*真的，这样的否定语句使用逻辑否定运算符 <code>~</code> 来表达。</p>
<p>当我们假设了矛盾存在时，就能推出任何命题。 遵循这一直觉，我们可以可以将 ~ P（即非 P）定义为 ∀ Q, P → Q。</p>
<p>不过 Coq 选择了稍有些不同（但等价）的做法，它将 ~ P 定义为 P → False，而 False 是在标准库中特别定义的矛盾性命题。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Module NotPlayground.</span><br><span class="line"></span><br><span class="line">Definition not (P:Prop) := P -&gt; False.</span><br><span class="line">Notation &quot;~ x&quot; := (not x) : type_scope.</span><br><span class="line">Check not : Prop -&gt; Prop.</span><br><span class="line">Check False.</span><br><span class="line"></span><br><span class="line">End NotPlayground.</span><br></pre></td></tr></table></figure>

<p>由于 False 是个矛盾性命题，因此爆炸原理对它也适用。如果我们让 False 进入到了证明的上下文中，可以对它使用 destruct 来完成任何待证目标。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Theorem ex_falso_quodlibet : forall (P:Prop),</span><br><span class="line">  False -&gt; P.</span><br><span class="line">Proof.</span><br><span class="line">  (* WORKED IN CLASS *)</span><br><span class="line">  intros P contra.</span><br><span class="line">  destruct contra.  </span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>不等性是十分常见的否定句的例子，，它有一个特别的记法 x ≠ y：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Notation &quot;x &lt;&gt; y&quot; := (~(x = y)).</span><br></pre></td></tr></table></figure>

<p>由于用 <code>ex_falso_quodlibet</code> 推理十分常用，因此 Coq 提供了内建的策略 <code>exfalso</code>。</p>
<p>由于不等性包含一个否定，因此在能够熟练地使用它前还需要一些练习。 这里有个有用的技巧：如果你需要证明某个目标不可能时（例如当前的目标陈述为 false &#x3D; true），请使用 <code>ex_falso_quodlibet</code> 将该目标转换为 False。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br></pre></td><td class="code"><pre><span class="line">Theorem not_true_is_false : forall b : bool,</span><br><span class="line">  b &lt;&gt; true -&gt; b = false.</span><br><span class="line">Proof.</span><br><span class="line">  intros b H.</span><br><span class="line">  destruct b eqn:HE.</span><br><span class="line">  - (* b = true *)</span><br><span class="line">    unfold not in H.</span><br><span class="line">    apply ex_falso_quodlibet.</span><br><span class="line">    apply H. reflexivity.</span><br><span class="line">  - (* b = false *)</span><br><span class="line">    reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<h3 id="4-真值"><a href="#4-真值" class="headerlink" title="4. 真值"></a>4. 真值</h3><p>与经常使用的 False 不同，True 很少使用，因为它作为证明目标来说过于平凡， 而作为前提又不携带任何有用的信息</p>
<h3 id="5-逻辑等价"><a href="#5-逻辑等价" class="headerlink" title="5. 逻辑等价"></a>5. 逻辑等价</h3><p>联结词“当且仅当”用起来十分方便，它是两个蕴含式的合取， 断言了两个命题拥有同样的真值</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Definition iff (P Q : Prop) := (P -&gt; Q) /\ (Q -&gt; P).</span><br><span class="line"></span><br><span class="line">Notation &quot;P &lt;-&gt; Q&quot; := (iff P Q)</span><br><span class="line">                      (at level 95, no associativity)</span><br><span class="line">                      : type_scope.</span><br><span class="line"></span><br><span class="line">End IffPlayground.</span><br></pre></td></tr></table></figure>



<h3 id="6-广集与逻辑等价"><a href="#6-广集与逻辑等价" class="headerlink" title="6. 广集与逻辑等价"></a>6. 广集与逻辑等价</h3><p>“广集（Setoid）”指配备了等价关系的集合，即满足自反性、对称性和传递性的关系。 当一个集合中的两个元素在这种关系上等价时，可以用 rewrite 将其中一个元素替换为另一个。为了开启此行为，我们需要导入 Coq 库来支持它：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">From Coq Require Import Setoids.Setoid.</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br></pre></td><td class="code"><pre><span class="line">Lemma mul_eq_0 : forall n m, n * m = 0 &lt;-&gt; n = 0 \/ m = 0.</span><br><span class="line">Theorem or_assoc : forall P Q R : Prop, P \/ (Q \/ R) &lt;-&gt; (P \/ Q) \/ R.</span><br><span class="line"></span><br><span class="line">Lemma mul_eq_0_ternary :</span><br><span class="line">  forall n m p, n * m * p = 0 &lt;-&gt; n = 0 \/ m = 0 \/ p = 0.</span><br><span class="line">Proof.</span><br><span class="line">  intros n m p.</span><br><span class="line">  rewrite mul_eq_0. rewrite mul_eq_0. rewrite or_assoc.</span><br><span class="line">  reflexivity.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>



<h3 id="7-存在量化"><a href="#7-存在量化" class="headerlink" title="7. 存在量化"></a>7. 存在量化</h3><p>*’存在量化’*也是十分重要的逻辑联结词。我们说存在某个类型为 T 的 x，使得某些性质 P 对于 x 成立，写作 ∃ x : T, P。</p>
<p>为了证明形如 ∃ x, P 的语句，我们必须证明 P 对于某些特定的 x 成立，这些特定的 x 被称作存在性的*’例证’*。</p>
<ul>
<li>首先，我们调用 ∃ t 策略向 Coq 指出已经知道了使 P 成立的例证 t</li>
<li>然后证明将所有出现的 x 替换成 t 的命题 P</li>
</ul>
<p>如果我们的的上下文中有形如 ∃ x, P 的存在前提， 可以将其解构得到一个例证 x 和一个陈述 P 对于 x 成立的前提。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Theorem exists_example_2 : forall n,</span><br><span class="line">  (exists m, n = 4 + m) -&gt;</span><br><span class="line">  (exists o, n = 2 + o).</span><br><span class="line">Proof.</span><br><span class="line">  (* WORKED IN CLASS *)</span><br><span class="line">  intros n [m Hm]. </span><br><span class="line">  exists (2 + m).</span><br><span class="line">  apply Hm.  Qed.</span><br></pre></td></tr></table></figure>



<h2 id="使用命题编程"><a href="#使用命题编程" class="headerlink" title="使用命题编程"></a>使用命题编程</h2><p>逻辑联结词，使得我们能够用简单命题去构造复杂命题，例如定义函数返回一个命题：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint In &#123;A : Type&#125; (x : A) (l : list A) : Prop :=</span><br><span class="line">  match l with</span><br><span class="line">  | [] =&gt; False</span><br><span class="line">  | x&#x27; :: l&#x27; =&gt; x&#x27; = x \/ In x l&#x27;</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<p>虽然递归定义命题在某些情况下会很方便，但这种方式也有其劣势。特别是， 这类命题会受到 Coq 对递归函数要求的限制，例如，在 Coq 中递归函数必须是 “明显会终止”的。</p>
<h2 id="对参数应用定理"><a href="#对参数应用定理" class="headerlink" title="对参数应用定理"></a>对参数应用定理</h2><p>Coq 不同于其它证明助理（如 ACL2 和 Isabelle）的一个特性是， 它将*’证明’*本身也作为一等对象。</p>
<p>我们已经知道 Check 命令可以用来显式表达式的类型了， 不过它还可以用来查找某个标识符所指代的定理。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">Check plus     : nat -&gt; nat -&gt; nat.</span><br><span class="line">Check add_comm : forall n m : nat, n + m = m + n.</span><br></pre></td></tr></table></figure>

<p>在检查定理 plus_comm 的*’陈述’<em>时，Coq 使用了与检查某项的</em>‘类型’*一样的方式 （如果我们保留以冒号开始的部分，那么它会被打印出来）。这是为什么？</p>
<p>原因在于标识符 plus_comm 其实指代的是被称作*’证明对象’<em>的数据结构， 它表示在命题 ∀ n m : nat, n + m &#x3D; m + n 的真实性上建立的逻辑推导。 此对象的类型</em>‘就是’*其所证命题的陈述。</p>
<p>例如，若我们有一个类型为 nat → nat → nat 的项，就可以给它两个 nat 作为参数并得到一个 nat。 类似地，如果我们有一个类型为 n &#x3D; m → n + n &#x3D; m + m 的对象， 就能为它提供一个类型为 n &#x3D; m 的“参数”并推导出 n + n &#x3D; m + m。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br><span class="line">24</span><br><span class="line">25</span><br><span class="line">26</span><br><span class="line">27</span><br><span class="line">28</span><br><span class="line">29</span><br><span class="line">30</span><br><span class="line">31</span><br><span class="line">32</span><br><span class="line">33</span><br><span class="line">34</span><br><span class="line">35</span><br><span class="line">36</span><br><span class="line">37</span><br><span class="line">38</span><br><span class="line">39</span><br><span class="line">40</span><br><span class="line">41</span><br><span class="line">42</span><br><span class="line">43</span><br></pre></td><td class="code"><pre><span class="line">Lemma in_not_nil_42 :</span><br><span class="line">  forall l : list nat, In 42 l -&gt; l &lt;&gt; [].</span><br><span class="line">Proof.</span><br><span class="line">  intros l H.</span><br><span class="line">  Fail apply in_not_nil.</span><br><span class="line">Abort.</span><br><span class="line"></span><br><span class="line">(** There are several ways to work around this: *)</span><br><span class="line"></span><br><span class="line">(** Use [apply ... with ...] *)</span><br><span class="line">Lemma in_not_nil_42_take2 :</span><br><span class="line">  forall l : list nat, In 42 l -&gt; l &lt;&gt; [].</span><br><span class="line">Proof.</span><br><span class="line">  intros l H.</span><br><span class="line">  apply in_not_nil with (x := 42).</span><br><span class="line">  apply H.</span><br><span class="line">Qed.</span><br><span class="line"></span><br><span class="line">(** Use [apply ... in ...] *)</span><br><span class="line">Lemma in_not_nil_42_take3 :</span><br><span class="line">  forall l : list nat, In 42 l -&gt; l &lt;&gt; [].</span><br><span class="line">Proof.</span><br><span class="line">  intros l H.</span><br><span class="line">  apply in_not_nil in H.</span><br><span class="line">  apply H.</span><br><span class="line">Qed.</span><br><span class="line"></span><br><span class="line">(** Explicitly apply the lemma to the value for [x]. *)</span><br><span class="line">Lemma in_not_nil_42_take4 :</span><br><span class="line">  forall l : list nat, In 42 l -&gt; l &lt;&gt; [].</span><br><span class="line">Proof.</span><br><span class="line">  intros l H.</span><br><span class="line">  apply (in_not_nil nat 42).</span><br><span class="line">  apply H.</span><br><span class="line">Qed.</span><br><span class="line"></span><br><span class="line">(** Explicitly apply the lemma to a hypothesis. *)</span><br><span class="line">Lemma in_not_nil_42_take5 :</span><br><span class="line">  forall l : list nat, In 42 l -&gt; l &lt;&gt; [].</span><br><span class="line">Proof.</span><br><span class="line">  intros l H.</span><br><span class="line">  apply (in_not_nil _ _ _ H).</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>



<h2 id="Coq-vs-构造逻辑"><a href="#Coq-vs-构造逻辑" class="headerlink" title="Coq vs. 构造逻辑"></a>Coq vs. 构造逻辑</h2><h3 id="1-函数的外延性"><a href="#1-函数的外延性" class="headerlink" title="1. 函数的外延性"></a>1. 函数的外延性</h3><p>由于 Coq 的相等关系运算符是多态的， 因此我们可以在*’任何’<em>类型上使用它。特别是，我们可以写出断言</em>‘两个函数相等’*的命题</p>
<p>在一般的数学研究中，对于任意两个函数 f 和 g， 只要它们对相同的输入产生相等的结果，那么它们就被认为相等：</p>
<p>  (∀ x, f x &#x3D; g x) → f &#x3D; g</p>
<p>这被称作*’函数的外延性原理’*。</p>
<p>然而，函数的外延性并不在 Coq 的基本公理之内，因此某些“合理”的命题是不可证明的，不过我们可以用 Axiom 指令将函数的外延性添加到 Coq 的核心逻辑系统中。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Axiom functional_extensionality : ∀ &#123;X Y: Type&#125;</span><br><span class="line">                                    &#123;f g : X → Y&#125;,</span><br><span class="line">  (∀ (x:X), f x = g x) → f = g.</span><br></pre></td></tr></table></figure>

<p>将某个东西用 Axiom 定义为公理的效果与陈述一个定理并用 Admitted 跳过其证明相同， 不过它会提醒读者这是一个公理，我们无需证明！</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br></pre></td><td class="code"><pre><span class="line">Example function_equality_ex2 :</span><br><span class="line">  (fun x ⇒ plus x 1) = (fun x ⇒ plus 1 x).</span><br><span class="line">Proof.</span><br><span class="line">  apply functional_extensionality. intros x.</span><br><span class="line">  apply plus_comm.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>我们可以用Print Assumptions 指令查看某个证明依赖的所有附加公理</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br></pre></td><td class="code"><pre><span class="line">Print Assumptions function_equality_ex2.</span><br><span class="line">(* ===&gt;</span><br><span class="line">     Axioms:</span><br><span class="line">     functional_extensionality :</span><br><span class="line">         forall (X Y : Type) (f g : X -&gt; Y),</span><br><span class="line">                (forall x : X, f x = g x) -&gt; f = g *)</span><br></pre></td></tr></table></figure>



<h3 id="2-命题-vs-布尔值"><a href="#2-命题-vs-布尔值" class="headerlink" title="2. 命题 vs. 布尔值"></a>2. 命题 vs. 布尔值</h3><p>在 Coq 中有两种编码逻辑事实的方式，即使用*’布尔值’* （类型为 bool）和*’命题’*（类型为 Prop）。</p>
<table>
<thead>
<tr>
<th></th>
<th>bool</th>
<th>Prop</th>
</tr>
</thead>
<tbody><tr>
<td>decidable?</td>
<td>yes</td>
<td>no</td>
</tr>
<tr>
<td>useable with match?</td>
<td>yes</td>
<td>no</td>
</tr>
<tr>
<td>equalities rewritable?</td>
<td>no</td>
<td>yes</td>
</tr>
</tbody></table>
<p>这二者最本质的区别在于可判断性。<code>bool</code>是具体的，只有两个固定的值，而<code>Prop</code>是泛化的，<code>Prop</code>类型的值可以代表一个可证明的命题，也可以代表一个无法证明的命题。</p>
<p>第二行是直接从这个本质区别出发的。要计算布尔值上的模式匹配(或条件匹配)，我们需要知道被检查者的计算结果是真还是假;这只适用于bool，而不是Prop。</p>
<p>第三行突出了另一个重要的实际区别:像eqb_nat这样返回布尔值的相等函数不能直接用于证明重写是正确的，而命题eq则可以。</p>
<p>由于Prop包含可决定和不可决定的属性，当我们想要形式化一个恰好是可决定的属性时，我们有两种选择:我们可以将其表示为布尔计算或表示为Prop中的函数。</p>
<p>例如，我们可以通过以下两种方式来断言 n 为偶数：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">Example even_42_bool : evenb 42 = true.</span><br><span class="line">Proof. reflexivity. Qed.</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">Example even_42_prop : even 42.</span><br><span class="line">Proof. unfold even. ∃ 21. reflexivity. Qed.</span><br></pre></td></tr></table></figure>

<p>然而，即便布尔值和命题式在逻辑上是等价的， 但它们的方便性从某些特定的目上来看并不一样。</p>
<ul>
<li><p>无法在函数的定义中测试一般的命题是否为真，原因与 Coq 核心语言的*’可计算性’*特质有关, 因此，在 Coq 中 Prop *’并没有’*一种通用的情况分析操作来确定 任意给定的命题是否为真，一旦存在这种操作，我们就能写出不可计算的函数</p>
</li>
<li><p>通过布尔值来陈述事实会带来一点重要的优势，即通过对 Coq 中的项进行计算可以实现一些自动推理，这种技术被称为*’互映证明（Proof by Reflection）’*</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">Example even_1000&#x27; : evenb 1000 = true.</span><br><span class="line">Proof. reflexivity. Qed.</span><br></pre></td></tr></table></figure>
</li>
<li><p>布尔事实”的否定可以被直白地陈述并证明， 只需翻转预期的布尔值结果即可</p>
</li>
</ul>
<h3 id="3-经典逻辑-vs-构造逻辑"><a href="#3-经典逻辑-vs-构造逻辑" class="headerlink" title="3. 经典逻辑 vs. 构造逻辑"></a>3. 经典逻辑 vs. 构造逻辑</h3><p>在定义 Coq 函数时是无法判断命题 P 是否成立。 然而*’证明’*也存在类似的限制！</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">Definition excluded_middle := ∀ P : Prop,</span><br><span class="line">  P ∨ ¬ P.</span><br></pre></td></tr></table></figure>

<p>在证明形如 P ∨ Q 的陈述时，我们使用了 left 与 right 策略，它们能够有效地知道析取的哪边成立。然而，在 excluded_middle 中，P 是被全称量化的*’任意’*命题，我们对它一无所知。 我们没有足够的信息来选择使用 left 或 right 中的哪一个。</p>
<p>然而，如果我们恰好知道 P 与某个布尔项互映，那么就能很轻易地知道它是否成立了： 我们只需检查 b 的值即可。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Theorem restricted_excluded_middle : ∀ P b,</span><br><span class="line">  (P ↔ b = true) → P ∨ ¬ P.</span><br><span class="line">Proof.</span><br><span class="line">  intros P [] H.</span><br><span class="line">  - left. rewrite H. reflexivity.</span><br><span class="line">  - right. rewrite H. intros contra. discriminate contra.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>一般的排中律在 Coq 中默认并不可用，因为它是常见的逻辑系统（如 ZFC）中的标准特性。尽管如此，不假设排中律的成立仍有其独特的优点： Coq 中的陈述可以构造出比标准数学中同样陈述更强的断言。特别是， 当存在 ∃ x, P x 的 Coq 证明时，我们可以直接给出一个使 P x 得证的值 x。换言之，任何关于存在性的证明必定是*’构造性’*的。</p>
<p>像 Coq 一样不假设排中律成立的逻辑系统被称作*’构造逻辑’*。</p>
<p>像 ZFC 这样更加传统的，排中律对于任何命题都成立的逻辑系统则被称作*’经典逻辑’*。</p>
<blockquote>
<p>排中律是一个数理逻辑中的原理，它指出对于任意命题 P，P 或者成立，或者不成立，没有中间值。换句话说，排中律断定对于任意命题 P，P ∨ ¬P 恒为真。</p>
<p>在 Coq 中，排中律可以表示为 <code>excluded_middle</code> 假设，它的类型为 <code>forall P : Prop, P \/ ~P</code>，意味着任意一个命题 P，P 或者 ¬P 成立。</p>
<p>排中律的引入允许我们在证明中使用两种情况的分析，即假设 P 成立和假设 ¬P 成立，并根据这两种情况进行推理。</p>
<p>然而，需要注意的是，排中律在某些情况下可能会导致不可判定或无限推理的问题。因此，在使用排中律时需要谨慎，并考虑是否真正需要使用排中律来证明目标。</p>
</blockquote>
<p>即便构造逻辑很有用，它也有自身的限制：存在很多容易用经典逻辑证明的命题， 用构造证明只会更加复杂，而对于某些已知的命题而言这样的构造性证明甚至不存在！ 幸运的是，排中律和函数外延性一样都是与 Coq 的逻辑系统兼容的， 我们可以安全地将它作为公理添加到 Coq 中。然而，在本书中我们不必如此： 我们所涉及的结构都可以完全用构造逻辑得到，所需的额外代价则微不足道。</p>

    </div>

    
    
    

    <footer class="post-footer">

        

          <div class="post-nav">
            <div class="post-nav-item">
                <a href="/blog/2023/07/19/SF-1-Tactics/" rel="prev" title="SF-1-Tactics">
                  <i class="fa fa-chevron-left"></i> SF-1-Tactics
                </a>
            </div>
            <div class="post-nav-item">
                <a href="/blog/2023/09/09/Verilog/" rel="next" title="Verilog">
                  Verilog <i class="fa fa-chevron-right"></i>
                </a>
            </div>
          </div>
    </footer>
  </article>
</div>






</div>
  </main>

  <footer class="footer">
    <div class="footer-inner">


<div class="copyright">
  &copy; 
  <span itemprop="copyrightYear">2023</span>
  <span class="with-love">
    <i class="fa fa-heart"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">yanlw</span>
</div>
<div class="busuanzi-count">
    <span class="post-meta-item" id="busuanzi_container_site_uv">
      <span class="post-meta-item-icon">
        <i class="fa fa-user"></i>
      </span>
      <span class="site-uv" title="总访客量">
        <span id="busuanzi_value_site_uv"></span>
      </span>
    </span>
    <span class="post-meta-item" id="busuanzi_container_site_pv">
      <span class="post-meta-item-icon">
        <i class="fa fa-eye"></i>
      </span>
      <span class="site-pv" title="总访问量">
        <span id="busuanzi_value_site_pv"></span>
      </span>
    </span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io/" rel="noopener" target="_blank">Hexo</a> & <a href="https://theme-next.js.org/pisces/" rel="noopener" target="_blank">NexT.Pisces</a> 强力驱动
  </div>

    </div>
  </footer>

  
  <div class="reading-progress-bar"></div>

  <a href="https://gitee.com/yanlwsometing" class="github-corner" title="在 GitHub 上关注我" aria-label="在 GitHub 上关注我" rel="noopener" target="_blank"><svg width="80" height="80" viewBox="0 0 250 250" aria-hidden="true"><path d="M0,0 L115,115 L130,115 L142,142 L250,250 L250,0 Z"></path><path d="M128.3,109.0 C113.8,99.7 119.0,89.6 119.0,89.6 C122.0,82.7 120.5,78.6 120.5,78.6 C119.2,72.0 123.4,76.3 123.4,76.3 C127.3,80.9 125.5,87.3 125.5,87.3 C122.9,97.6 130.6,101.9 134.4,103.2" fill="currentColor" style="transform-origin: 130px 106px;" class="octo-arm"></path><path d="M115.0,115.0 C114.9,115.1 118.7,116.5 119.8,115.4 L133.7,101.6 C136.9,99.2 139.9,98.4 142.2,98.6 C133.8,88.0 127.5,74.4 143.8,58.0 C148.5,53.4 154.0,51.2 159.7,51.0 C160.3,49.4 163.2,43.6 171.4,40.1 C171.4,40.1 176.1,42.5 178.8,56.2 C183.1,58.6 187.2,61.8 190.9,65.4 C194.5,69.0 197.7,73.2 200.1,77.6 C213.8,80.2 216.3,84.9 216.3,84.9 C212.7,93.1 206.9,96.0 205.4,96.6 C205.1,102.4 203.0,107.8 198.3,112.5 C181.9,128.9 168.3,122.5 157.7,114.1 C157.9,116.9 156.7,120.9 152.7,124.9 L141.0,136.5 C139.8,137.7 141.6,141.9 141.8,141.8 Z" fill="currentColor" class="octo-body"></path></svg></a>

<noscript>
  <div class="noscript-warning">Theme NexT works best with JavaScript enabled</div>
</noscript>


  
  <script src="https://cdnjs.cloudflare.com/ajax/libs/animejs/3.2.1/anime.min.js" integrity="sha256-XL2inqUJaslATFnHdJOi9GfQ60on8Wx1C2H8DYiN1xY=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.6.4/jquery.min.js" integrity="sha256-oP6HI9z1XaZNBrJURtCoUT5SUnxFr8s3BzRl+cbzUq8=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.js" integrity="sha256-yt2kYMy0w8AbtF89WXb2P1rfjcP/HTHLT7097U8Y5b8=" crossorigin="anonymous"></script>
<script src="/blog/js/comments.js"></script><script src="/blog/js/utils.js"></script><script src="/blog/js/next-boot.js"></script>

  


  <script src="/blog/js/third-party/fancybox.js"></script>



  
  <script async src="https://busuanzi.ibruce.info/busuanzi/2.3/busuanzi.pure.mini.js"></script>





</body>
</html>
